%The following definitions mirror those of Garralda et al. \todo{Do we also distinguish between pre- and processes?}
%
%We say that a process $P$ is a \emph{communicating} process over channel $c$ if $P$ is one of the following:
%$$
%\begin{array}{rclcrcl}
%(1) & & c(x:\capab).P & \qquad& (2) & & \outC{c}{v}.P \\
%(3) & & \branch{c}{n:P \dots n:P} & & (4) & & \select{c}{n}.P \\
%(5) & & \close{c}.P & &  & & 
%\end{array}
%$$
%Two communicating processes are \emph{dual} of each other if they are, respectively, of the forms (1) and (2), 
%(3) and (4), or a pair of (5), as given above.
%
%We say that sessions are \emph{safe} because they are not disrupted by a reconfiguration step.
%That is, the execution of such a step does not affect the communication potential of a session.
%Below, we write $\pired_r$ to stand for a reconfiguration step, i.e., a reduction inferred using rule $\rulename{r:Upd}$.
%
%\begin{definition}[Safe session]
%A session is safe in a process $P$ if $P \pired^{*} P' \equiv E[C[R] \parallel D[Q]] $,
%where $R$ and $Q$ are dual communicating processes in that session, and $P' \pired_r P''$
%imply $P'' \equiv E'[C'[R] \parallel D'[Q]]$, for some contexts $E', C', D'$.
%\end{definition}